#include "bdd.h"
int main(void)
{
	BDD _bddk;
	BDD _bddb;
	BDD _bddc;
	BDD _bddl;
	BDD _bdde;
	BDD _bddp;
	BDD _bddh;
	BDD _bdda;
	BDD _bddg;
	BDD _bddd;
	BDD _bddj;
	BDD _bddf;
	BDD _bddt;
	BDD _bddi;
	BDD _bddo;
	BDD _bddm;
	BDD _bddr;
	BDD _bddn;
	BDD _bddu;
	BDD _bddq;
	BDD _bddv;
	BDD _bdds;
        double d1, d2;

	bdd_init(1000,1000);
	bdd_varnum();
	bdd_setvarnum(4);
	_bdda = bdd_makeset((int []) { 0,1,2,3,},4);
	_bdda = bdd_addref(_bdda);
	_bddb = bdd_nithvar(0);
	_bddb = bdd_addref(_bddb);
	_bddb = bdd_apply(bddtrue,_bddb,0);
	_bddb = bdd_addref(_bddb);
	_bddb = bdd_delref(_bddb);
	_bddc = bdd_ithvar(1);
	_bddc = bdd_addref(_bddc);
	_bddd = bdd_apply(_bddb,_bddc,0);
	_bddd = bdd_addref(_bddd);
	_bddb = bdd_delref(_bddb);
	_bddc = bdd_delref(_bddc);
	_bdde = bdd_ithvar(2);
	_bdde = bdd_addref(_bdde);
	_bddf = bdd_apply(_bddd,_bdde,0);
	_bddf = bdd_addref(_bddf);
	_bddg = bdd_delref(_bddd);
	_bdde = bdd_delref(_bdde);
	_bddh = bdd_nithvar(3);
	_bddh = bdd_addref(_bddh);
	_bddi = bdd_apply(_bddf,_bddh,0);
	_bddi = bdd_addref(_bddi);
	_bddj = bdd_delref(_bddf);
	_bddh = bdd_delref(_bddh);
	_bddk = bdd_ithvar(0);
	_bddk = bdd_addref(_bddk);
	_bddk = bdd_apply(bddtrue,_bddk,0);
	_bddk = bdd_addref(_bddk);
	_bddk = bdd_delref(_bddk);
	_bddl = bdd_nithvar(1);
	_bddl = bdd_addref(_bddl);
	_bddm = bdd_apply(_bddk,_bddl,0);
	_bddm = bdd_addref(_bddm);
	_bddk = bdd_delref(_bddk);
	_bddl = bdd_delref(_bddl);
	_bdde = bdd_ithvar(2);
	_bdde = bdd_addref(_bdde);
	_bddn = bdd_apply(_bddm,_bdde,0);
	_bddn = bdd_addref(_bddn);
	_bddo = bdd_delref(_bddm);
	_bdde = bdd_delref(_bdde);
	_bddp = bdd_ithvar(3);
	_bddp = bdd_addref(_bddp);
	_bddq = bdd_apply(_bddn,_bddp,0);
	_bddq = bdd_addref(_bddq);
	_bddr = bdd_delref(_bddn);
	_bddp = bdd_delref(_bddp);
	_bdds = bdd_apply(_bddi,_bddq,2);
	_bdds = bdd_addref(_bdds);
	_bddt = bdd_delref(_bddi);
	_bddu = bdd_delref(_bddq);
	_bdda = bdd_addref(_bdda);
	d1 = bdd_satcountset(_bdds,_bdda);
	bdd_setvarnum(20);
	d2 = bdd_satcountset(_bdds,_bdda);
	_bddv = bdd_delref(_bdds);
	_bdda = bdd_delref(_bdda);
        printf("%.3lf = %.3lf\n", d1, d2);
        return 0;
}
